「現在，世上已經有能思考、能學習，也能創造的機器。」
—— 赫伯特・西蒙與艾倫・紐厄爾，1958 年論文，節譯。

想像你正在改數學考卷。

有個學生交上來的證明，跟課本不一樣，而且短了一截。你心想，這傢伙又在省略步驟，拿起紅筆，準備找出他跳過了哪裡。

結果，第一行沒問題，第二行也成立。一路檢查到最後，居然真的接得上。

他不是漏寫，而是少繞了一段路。

你只好把紅筆放下。

現在，把這個學生換成 AI，你還會這麼乾脆給它分數嗎？還是會多看兩眼，懷疑它用了什麼看似合理、其實根本不成立的說法？

同樣是沒看過的解法，怎麼分辨它是新發現，還是亂掰？

今天這個故事，就從一份跟書上不一樣的證明開始。

這次，不准照解答抄

1950 年代，紐厄爾、西蒙與程式設計師蕭（Cliff Shaw），一起開發了「邏輯理論機」（Logic Theorist）。

上一篇提到，他們挑中的考卷，是懷海德與羅素合著的《數學原理》。

他們要電腦處理的，不是加減乘除，而是書裡的邏輯定理。這類題目最麻煩的地方，是你不能只說答案是什麼，還得交代它為什麼成立。

把結論抄一次，前面加上「顯然可知」，通常不會比較有幫助。

研究者先把公理、可用的定理與推理規則，整理成程式能處理的形式，再交給它一個要證明的命題。

但完整解法，沒有一起附上。

你可以把它想成：工具都擺在桌上了，目標也告訴你了。至於先用哪個、怎麼接起來，自己找。

這才是他們真正想測試的事。

電腦不只要照著步驟做，還得設法找出步驟。

它沒開悟，只是知道哪些地方值得先找

問題是，每一步都有不同的走法。全部試過，聽起來很公平，實際上卻可能忙了半天，還在跟題目無關的地方打轉。

就像數學考卷寫滿了公式，最後那一行，始終接不到答案。

所以，研究者替程式安排了一些引導搜尋的方法，讓它優先嘗試比較有希望的方向。這類方法，叫做啟發式方法。

例如，現在要證明 C，手上剛好有一條規則：「只要 B 成立，就能推出 C。」

那就先別死盯著 C，改去找 B 的證明。找到以後，再把兩段接起來；這條路走不通，就嘗試別的方向。

它不保證每次成功，但至少不用對每一條岔路都同樣執著。

1957 年的實驗報告記錄，邏輯理論機找出了《數學原理》第二章前 52 道定理中，38 道的證明。

而它最出名的成果之一，是替第 2.85 號定理，找到了比原書更簡潔的證明。

所以，上一篇那份「標準答案」，到底出了什麼問題？

其實沒有。

原書的證明成立，機器找到的另一種證明也成立。只是抵達同一個結論，不一定要走同一條路。

這裡值得興奮的，不是電腦打敗了哪位數學家，而是研究者沒有把這份新解法逐行寫給它，它仍然找到了。

但別忘了，故事還有另外一半。

我們之所以能稱它為「新解法」，而不是「新錯法」，是因為那份證明經得起檢查。

找出一條路，和確認這條路走得通，是兩件事。

AI 可以找答案，但「找到了」不能只靠它自己說

把時間拉回近年的 AI 研究。

Google DeepMind 在 2024 年公布的 AlphaProof，也要處理數學證明。不過，它不是把邏輯理論機換台電腦再跑一次，而是結合神經網路、強化學習與搜尋，學習哪些證明步驟值得嘗試。

同時，它還有一個重要搭檔：Lean。

Lean 是一套形式化證明工具。先不用被名字嚇到，你可以把它想成一位只認規則、不吃口才那套的閱卷老師。

AlphaProof 嘗試尋找證明，Lean 則依照明確的形式規則，檢查產生的證明能不能成立。

不是另一個聊天機器人看完以後說：「嗯，我也覺得很有道理。」

更不是在結尾補一句「我非常確定」，就算交卷成功。

搜尋過程中，AlphaProof 可以試錯、走進死路，再回頭找其他方法。但一份要被接受的完整證明，不能靠省略關鍵步驟混過去。

這就是它和聊天視窗裡一大段流暢解釋的差別。

解釋可以幫助我們理解想法，卻不會因為寫得完整、語氣篤定，就自動通過驗證。

當然，Lean 也不是什麼都知道。它核對的是已經形式化的命題；假如一開始就把題目翻錯，它仍可能很嚴謹地驗證了另一道題。

它讓一部分錯誤有了明確的檢查方式，沒有讓所有問題從此消失。

放回寫程式的情境，其實很好理解。

假設 AI 告訴你：「問題已經修好了。」

你真正想看的，應該是原本出錯的操作能不能正常完成、測試有沒有通過，而不是它把「修好了」再講得更有自信。

測試通過不等於沒有任何 bug，更不等於數學上的完整證明。但至少，那是完成宣言之外，可以拿來檢查的證據。

回頭看那份比原書簡潔的解法，道理也是一樣。

值得相信的，不是它敢跟課本寫得不一樣。

而是寫得不一樣，依然每一步都站得住腳。

接著，他們不想只做數學題了

先把時間留在那群剛讓電腦找出證明的人身上。

既然可以把目標拆成小問題，再一步步尋找解法，這種方法能不能搬到其他任務上？換一種題目，就一定得從頭寫一套程式嗎？

紐厄爾、西蒙與蕭開始嘗試，把通用的解題方法，和個別領域的知識分開。

接下來的系統，有了一個更有野心的名字。

General Problem Solver。

通用問題解決器。

不再只為某一類邏輯題服務。他們希望，同一套解題方法，換一組知識與規則，也能派上用場。

只是，這個計畫藏著一個前提。

人類必須先把目標、條件，以及允許採取的動作，整理成機器讀得懂的形式。

數學書早就替他們準備好了這些東西。離開書頁以後，誰來準備？

他們已經開始教機器找答案。

接下來才發現，更難交出去的，可能是題目本身。